COMMENT ⊗   VALID 00009 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the notion of multiplicity
C00006 00003	multiplicity of union is sum of multiplicities
C00008 00004	*-→proof of facts about mult
C00018 00005	mult_nthcdr
C00020 00006	lemma multiplicity implies injectivity: a sublemma
C00027 00007	lemma multiplicity implies injectivity
C00037 00008	proof multsum                                
C00041 00009	Lemma:if disjoint-set,then multiplicity of union = sum of the multiplicities
C00056 ENDMK
C⊗;
;the notion of multiplicity

(wipe-out)
(get-proofs sums prf ekl sys)

(proof multiplicity)

(decl mult (type: |(ground⊗@set)→ground|))
(defax mult |∀x u a.mult(nil,a)=0∧
                    mult(x.u,a)=if a(x) then mult(u,a)' else mult(u,a)|)
(label mult_def)

;facts about multiplicity

(axiom |∀u a.natnum(mult(u,a))|)
(label simpinfo)(label multfact)

(axiom |∀u a.mult(u,a)≤length(u)|)
(label length_mult)

(axiom |∀u y a.member(y,u)∧a(y)⊃1≤mult(u,a)|) 
(label member_mult)

;Exercise:(not used in the proofs)
;(axiom |∀a u x.mult(u,a)≤mult(x.u,a)|)
;(label simpinfo)(label multfact)

(axiom |∀a u n.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|)
(label mult_nthcdr)

(axiom |∀u.mult(u,emptyset)=0|)
(label simpinfo)(label emptyfacts)

(axiom |∀v i j.i<j∧j<length v∧nth(v,i)=nth(v,j)⊃
               2≤mult(v,mkset(nth(v,i)))|)
(label multinj_computation)

(axiom |∀v.(∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1)⊃inj(v)|)
(label mult_inj)
;multiplicity of union is sum of multiplicities
(proof mult_of_un_is_sum_un)

(axiom |∀u a b.disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|)
(label multsum)

(axiom |∀setseq u n.disjoint(setseq,n)⊃
                    mult(u,un(setseq,n))=sum(λm.mult(u,setseq(m)),n)|)
(label mult_of_un_is_sum_mult)
(save-proofs mult)
;*-→proof of facts about mult
    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multprop)
    (unlabel simpinfo multfact)

    (ue (phi |λu.∀a.natnum(mult(u,a))|) listinduction 
	(use mult_def mode: always))

    (label simpinfo multfact)

    ;not used later in the proofs
    ;(trw |∀a u x.mult(u,a)≤mult(x.u,a)| (open mult lesseq) (use successor1))
    ;∀A U X.mult(U,A)≤mult(X.U,A)

    ;multiplicity is lesseq length

    (ue (phi |λu.mult(u,a)≤length(u)|) listinduction 
	lesseq_lesseq_succ (open mult length) (part 1#1(open lesseq)))
    ;∀U.MULT(U,A)≤LENGTH U

    ;if there is a member, multiplicity is not zero

    (ue (phi |λu.∀y a.member(y,u)∧a(y)⊃0<mult(u,a)|) listinduction 
	(open mult member) (use normal mode: always))
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃0<MULT(U,A)

    (rw * use less_lesseqsucc mode: always))
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)

    ;mult emptyset
    (unlabel simpinfo emptyfacts)

    (ue (phi |λu.mult(u,emptyset)=0|) listinduction 
	(part 1(open emptyset mult)))
    ;∀U.MULT(U,EMPTYSET)=0
    (label simpinfo emptyfacts)
;mult_nthcdr

    ;we prepare a rewriter


    (ue ((q.|mult(nthcdr(u,n'),a)'≤mult(u,a)|)
	 (r.|mult(nthcdr(u,n'),a)≤mult(u,a)|)
	 (p.|a(nth(u,n))|)) trans_cond
	(use succ_lesseq_lesseq ue: ((m.|mult(nthcdr(u,n'),a)|)
				     (n.|mult(u,a)|)) mode: exact ))
    ;(IF A(NTH(U,N)) THEN MULT(NTHCDR(U,N'),A)'≤MULT(U,A)
    ;    ELSE MULT(NTHCDR(U,N'),A)≤MULT(U,A))⊃MULT(NTHCDR(U,N'),A)≤MULT(U,A)

    ;conclusion

    (ue (a |λn.∀a u.n<length(u)⊃mult(nthcdr(u,n),a)≤mult(u,a)|) proof_by_induction
	(part 1#1 (open nthcdr lesseq)) succ_less_less 
	(part 1#2#1#1 (use nthcdr_car_cdr mode: always)) (open mult)   *)
    ;∀N A U.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)

;lemma multiplicity implies injectivity: a sublemma
;to compute multiplicity

    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multinj_computation)

1.  (assume |j<length v|)
    (label mc0)

2.  (assume |i<j|)
    (label mc1)

3.  (assume |nth(v,i)=nth(v,j)|)
    (label mc2)

4.  (derive |i<length v| (mc0 mc1 transitivity_of_order))
    (label mc3)
    ;deps: (mc0 mc1)

    ;labels: NTH_IN_NTHCDR 
    ;(AXIOM |∀U N M.N≤M∧M<LENGTH U⊃MEMBER(NTH(U,M),NTHCDR(U,N))|)

5.  (ue ((u.v)(n.|i'|)(m.j)) nth_in_nthcdr mc0 mc1 
        (use less_lesseqsucc mode: exact direction: reverse))
    ;MEMBER(NTH(V,J),NTHCDR(V,I'))
    (label mc4)
    ;deps: (MC0 MC1)

    ;labels: MEMBER_MULT 
    ;∀U Y A.MEMBER(Y,U)∧A(Y)⊃1≤MULT(U,A)

6.  (ue ((u.|nthcdr(v,i')|)(y.|nth(v,j)|)(a.|mkset nth(v,j)|)) member_mult 
        (part 1(open lesseq mkset)) mc4
        (use mc2 mode: exact direction: reverse)) 
    ;1≤MULT(NTHCDR(V,I'),MKSET(NTH(V,I)))
    (label mc5)
    ;deps: (MC0 MC1 MC2)

7.  (trw |n≤mult(nthcdr(v,i'),mkset nth(v,i))⊃n'≤mult(nthcdr(v,i),mkset nth(v,i))| 
         (open mult mkset)(use nthcdr_car_cdr mc3 mode: exact))
    ;N≤MULT(NTHCDR(V,I'),MKSET(NTH(V,I)))⊃N'≤MULT(NTHCDR(V,I),MKSET(NTH(V,I)))
    ;deps: (MC0 MC1)

8.  (ue (n |1|) * mc5)
    ;2≤MULT(NTHCDR(V,I),MKSET(NTH(V,I)))
    (label mc6)
    ;deps: (MC0 MC1 MC2)

    ;labels: MULT_NTHCDR 
    ;(AXIOM |∀A U N.N<LENGTH U⊃MULT(NTHCDR(U,N),A)≤MULT(U,A)|)

9.  (ue ((n.i)(u.v)(a.|mkset nth(v,i)|)) mult_nthcdr mc3)
    ;MULT(NTHCDR(V,I),MKSET(NTH(V,I)))≤MULT(V,MKSET(NTH(V,I)))
    ;deps: (MC0 MC1)

    ;labels: TRANS_LESSEQ 
    ;∀N M K.N≤M∧M≤K⊃N≤K

10. (ue ((n.|2|)
         (m.|mult(nthcdr(v,i),mkset nth(v,i))|)
         (k.|mult(v,mkset nth(v,i))|))
        trans_lesseq mc6 *)

11. (ci (mc1 mc0 mc2))
    ;I<J∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃2≤MULT(V,MKSET(NTH(V,I)))
;lemma multiplicity implies injectivity
(proof mult_inj)

1.  (assume |∀k.k<length v⊃mult(v,mkset(nth(v,k)))=1|)
    (label mi1)

2.  (assume |i<length v∧j<length v∧nth(v,i)=nth(v,j)|)
    (label mi2)

3.  (ue ((v.v)(i.i)(j.j)) multinj_computation mi2
        (use mi1 ue: ((k.i)) mode: exact)(open lesseq))
    ;¬I<J
    ;deps: (MI1 MI2)

4.  (ue ((v.v)(i.j)(j.i)) multinj_computation mi2
        (use mi1 ue: ((k.j)) mode: exact)(open lesseq))
    ;¬J<I
    ;deps: (MI1 MI2)

5.  (derive |i=j| (trichotomy * -2))
    ;deps: (MI1 MI2)

6.  (ci mi2)
    ;I<LENGTH V∧J<LENGTH V∧NTH(V,I)=NTH(V,J)⊃I=J
    ;deps: (MI1)

7.  (trw |inj v| (open inj) *)
    ;INJ(V)
    ;deps: (MI1)

8.  (ci mi1)
    ;(∀K.K<LENGTH V⊃MULT(V,MKSET(NTH(V,K)))=1)⊃INJ(V)
;proof multsum                                
;Lemma:if disjoint union, the mult. of the union is the sum of the multiplicities

    (wipe-out)
    (get-proofs mult prf ekl sys)
    (proof multsum)

1.  (ue (phi |λu. disj_pair(a,b)⊃mult(u,a∪b)=mult(u,a)+mult(u,b)|) listinduction
	(part 1 (open mult union disj_pair emptyp intersection) 
		(use normal mode: always)) 
	    (part 1 (der)) )
    ;∀U.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)
    (label multsum)

;LEMMA
;∀U.DISJ_PAIR(A,B)⊃MULT(U,A∪B)=MULT(U,A)+MULT(U,B)

;Proof: By induction on U. For U = NIL, all values of mult are 0. Assume it for U,
;want it for X.U. The assumption that A and B are disjoint means that the intersection 
;of A and B is EMPTYP, i.e. that for no X, Xε A and XεB. If not XεA and not XεB
;then induction hypothesis gives the result. If XεA or XεB, then by disjointness
;if xεA then ¬xεB, else XεB and in both cases 
;mult(X.U,A∪B)=mult(U,A∪B)'=(mult(U,A)+mult(U,B))'=mult(X.U,A)+mult(X.U,B)
;(-the induction hypothesis is used to establish the second equality-)
;Lemma:if disjoint-set,then multiplicity of union = sum of the multiplicities

    (proof mult_of_un_is_sum_mult)

1.  (ue (a |λn.disjoint(setseq,n)⊃mult(u,un(setseq,n))=sum(λx1.mult(u,setseq(x1)),n)|)
	 proof_by_induction (open disjoint un sum mult ) multfact
	(use multsum mode: exact) (use normal mode: always))
    ;∀N.DISJOINT(SETSEQ,N)⊃MULT(U,UN(SETSEQ,N))=SUM(λX1.MULT(U,SETSEQ(X1)),N)



;LEMMA
;∀N.DISJOINT(SETSEQ,N)⊃mult(U,UN(SETSEQ,N))=SUM(λX1.mult(U,SETSEQ(X1)),N)

;Proof: By induction on N. For N=0, UN(SETSEQ,0) is EMPTYSET, whose mult in 0 (simpinfo),
;and SUM(...,0) is 0 too. Assume the result for N.
;DISJOINT(SETSEQ,N')
;                    implies
;DISJOINT(SETSEQ,N)
;                    By DISJOINTFACT, it follows 
;DISJ_PAIR(UN(SETSEQ,N),SETSEQ(N))      
;                    which implies, using multSUM
;mult(U,UN(SETSEQ,N)∪SETSEQ(N))=mult(U,UN(SETSEQ,N))+mult(U,SETSEQ(N))
;                    which is, by definition of UN and induction hypothesis
;mult(U,UN(SETSEQ,N'))=SUM(λX1.mult(U,SETSEQ(X1)),N)+mult(U,SETSEQ(N))
;                    i.e. by definition of sum
;mult(U,UN(SETSEQ,N'))=SUM(λX1.mult(U,SETSEQ(X1)),N')